qadd_grp  ocgrp{i:l} 

latex

Definitions

grp_inv(g), grp_id(g), inverse(T; op; id; inv), monot(T; x,y.R(x;y); f), cancel(T; S; op), r - s, True, T, guard(T), P  Q, P  Q, P  Q, P  Q, anti_sym(T; x,y.R(x;y)), trans(T; x,y.E(x;y)), refl(T; x,y.E(x;y)), connex(T; x,y.R(x;y)), order(T; x,y.R(x;y)), q_le(r; s), linorder(T; x,y.R(x;y)), t.2, t.1, grp_op(g), grp_le(g), qadd_grp, grp_car(g), abmonoid{i:l}, x,y. t(x;y), prop{i:l}, x:A. B(x), x f y, P  Q, ocmon{i:l}, ocgrp{i:l}, t  T, False, A, grp{i:l}, abgrp{i:l}, x(s1,s2), mon{i:l}, subtype(S; T)

Lemmas

qadd com, qadd minus, qinverse q, mon ident q, q trichotomy, qinv inv q, qinv thru op q, qminus positive, qadd inv assoc q, qadd ac 1 q, qadd comm q, mon assoc q, int inc rationals, qmul wf, qadd wf, bool wf, true wf, squash wf, qadd positive, q le wf, assert-qeq, or functionality wrt iff, assert of bor, qeq wf2, qsub wf, qpositive wf, bor wf, iff transitivity, rationals wf, abgrp wf, comm wf, qadd grp wf, monot wf, cancel wf, grp le wf, assert wf, linorder wf, grp inv wf, grp id wf, grp op wf, grp car wf, inverse wf